\begin{tabbing}
$\forall$${\it es}$:ES, ${\it ff}$:FIFO, ${\it f2f+}$:F2F+{-}decls.
\\[0ex]plus{-}ify\{i:l\}(${\it es}$;${\it ff}$;is\_req  ;is\_ack ;awaiting ;owes\_ack )
\\[0ex]$\Rightarrow$ \=($\forall$${\it sndr}$, ${\it rcvr}$:${\it ff}$.C, $e$:E.\+
\\[0ex][$e$: ${\it sndr}$ $\leftarrow$is\_ack $--$ ${\it rcvr}$]
\\[0ex]$\Rightarrow$ ($\exists$${\it e'}$:\{$a$:E$\mid$ [$a$: ${\it sndr}$ $--$is\_req  $\rightarrow$ ${\it rcvr}$]\} . f2f+{-}pred(${\it e'}$,${\it ff}$.Sender(${\it sndr}$,$e$))))
\-
\end{tabbing}